SAT solver

充足可能な場合は、その論理式を充足するような各変数に対する具体的な真偽値割当てを出力する

そうでない場合は充足不能である旨を知らせる

例

どういうアルゴリズムで解いてる？

GPT-4.icon

DPLLアルゴリズムは、古典的なSAT Solverのアルゴリズムの一つです。

このアルゴリズムは、変数の真偽値の割り当てを試行的に選択し、その選択が正しいかどうかを再帰的に検証します。

不適切な割り当てが見つかった場合、バックトラックして別の割り当てを試みます。

単一化規則や純粋リテラル規則などのヒューリスティックを用いて、探索の効率を向上させることができます。

このアルゴリズムは、不適切な変数の割り当てが見つかったときに、その原因となる節（コンフリクト節）を学習し、新しい節として追加します。

この学習により、同じエラーを繰り返すことなく、より効率的に探索空間を狭めることができます。

ランダム化と再スタート

探索の効率を向上させるために、ランダムに変数の割り当てを選択することがあります。

また、探索が停滞した場合には、探索を初めからやり直す「再スタート」を行うことで、新しい探索空間を試みることができます。

並列化とポートフォリオ

複数のコアやマシンを利用して、並列に探索を行うことで、計算時間を短縮するアプローチもあります。

ポートフォリオアプローチでは、複数の異なるアルゴリズムやヒューリスティックを組み合わせて、最も効果的なものを動的に選択します。